es{-}x{-}equiv(${\it es}$; $i$; $x$; $s_{1}$; $s_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$z$:Id. ($\neg$($z$ = $x$ $\in$ Id)) $\Rightarrow$ ($s_{1}$($z$) = $s_{2}$($z$) $\in$ es\_vartype(${\it es}$; $i$; $z$))